『Homotopy Type Theory Univalent Foundations of Mathematics』Chapter 1 Type theory

P17～P58

table:訳

witness 証拠？

membership メンバーシップ、所属性？

disprove 反証を挙げる

judgmental equality 判断的等号？、判断としての等しさ？

definitional equality 定義的等号？、定義としての等しさ？

A has proof

a : A 項aは型Aを持つ

aはAの点である(ホモトピー型理論)

参考